Inference at * 1 
Iof proof for Lemma neg mul arg bounds:



1. a : 
2. b : 
3. (((-a) * b) > 0)  ((((-a) > 0) & (b > 0))  (((-a) < 0) & (b < 0)))
  ((a * b) < 0)  (((a < 0) & (b > 0))  ((a > 0) & (b < 0))) 

latex

 by InteriorProof ((ReplaceWithEqv (TryC (HigherC IntSimpC)) 
 ((-(a * b)) > (-0))
 ((-(a * b)) > (-0 ((((-a) > (-0)) & (b > 0))  (((-a) < (-0)) & (b < 0))) 
 3) 

 3) CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
 3) )) (first_tok :t) inil_term))) 

latex

 1: 

 1: 3. ((-(a * b)) > (-0))  ((((-a) > (-0)) & (b > 0))  (((-a) < (-0)) & (b < 0)))
 1:   ((a * b) < 0)  (((a < 0) & (b > 0))  ((a > 0) & (b < 0)))
 .

Definitions	P  Q, T, P  Q, P  Q, , True, t  T, P & Q, P  Q, i > j, x:A. B(x)
Lemmas	true wf, squash wf, iff wf, gt wf